import gov.nasa.jpf.jvm.Verify;
import gov.nasa.jpf.symbc.Debug;



public class StrangeCalculator {
	
	private int magicValue = 36;
	
	public StrangeCalculator(){
		
	}
	
	public int add(int left, int right){
		
		boolean flag = false;
		
		if(left < 0){
			left = -left;
		}
		
		if(right > 100){
			flag = true;
Verify.ignoreIf(!flag);
			magicValue = 18; 
		}
		
		if(right <0){
			right = -right;
		}
		
		if(right > 100){
			magicValue = 18;
		}
		
		Verify.ignoreIf(!flag);
		
		return left + right + magicValue;
	}
	
	public int minus(int left, int right){
		if(left < 0){
			left = -left;
		}
		
		if(left > 50){
			magicValue = 36;
		}
		
		if(right < 0){
			right = -right;
		}
		
		if(right > left){
			right = 18;
		}
	
		return magicValue + left - right;
	}
	
	public int multiply(int left, int right){
		if(left < 0){
			left = -left;
		}
		
		if(left > 100){
			left = 100;
		}
		
		if(right <0){
			right = -right;
		}
		
		if(right > 100){
			right = 100;
		}
		
		return left * right * magicValue;
	}
	
	public int divide(int left, int right){
		if(left < 0){
			left = -left;
		}
		
		if(left <1000){
			magicValue = 18;
		}
		
		if(right < 0){
			right = -right;
		}
		
		if(right > 100){
			magicValue = 36;
		}
		
		return  (magicValue*left) / right;
	}
	
	public static void main(String[] args){
		StrangeCalculator sc = new StrangeCalculator();
		sc.add(-100, 100);
		sc.add(-1000000,101);
		sc.add(0,101);
		Debug.printPC("\nSc.add Path Condition: ");
	}
	
}
